Bit-Precise Reasoning with Affine Functions,” in Satisfiability Modulo Theories

The class of affine Boolean functions is rich enough to express constant bits and de-pendencies between different bits of different words. For example, the function (x0) ∧ (¬y1) ∧ (x4 ⇐ ⇒ y7) ∧ (x5 ⇐ ⇒ ¬y9) is affine and expresses the invariant that the low bit (bit 0) of the variable x is true, that bit 1 of y is false, that the bits 4 and 7 of x and y coincide whereas bits 5 and 9 of x and y differ. This class of Boolean function is amenable to bit-precise reasoning since it satisfies strong chain properties which bound the number of times a system of semantic fixpoint equations need to be reapplied when reasoning about loops. This paper address the key problem of abstracting an arbitrary Boolean function to either a general affine function or a so-called affine function of width 2, when the function is represented as an ROBDD. Novel algorithms are presented for this task: one that manipulates Boolean vectors and another which is inspired by anti-unification. The speed and precision of both algorithms are compared on benchmark circuits, to draw conclusions on the tractability of affine abstraction.